T:Type, f:(TT). retraction(T;f)  (L:(T List), x, y:T. x=f*(y) via L  no_repeats(T;L)) 

latex

Definitions

x:A  B(x), x:A. B(x), retraction(T;f), Type, t  T, s = t, x:AB(x), type List, y=f*(x) via L, no_repeats(T;l), P  Q, l[i], f(a), a < b, #$n, {i..j}, x:A. B(x), ||as||, , left + right, P  Q, , , A, <a, b>, False, P & Q, A  B, i  j < k, , {x:A| B(x)} , Void, |g|, S  T, A List, [car / cdr], i  j , (x  l), n+m, [], t  ...$L, x.A(x), {T}, x,y,z. t(x;y;z), SQType(T), s ~ t, Dec(P), Atom, b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, a < b, A c B, x f y, |r|, xL. P(x), (xL.P(x)), Unit, , hd(l), i <z j, i z j, n - m, P  Q, P  Q, -n, increasing(f;k), tl(l), L1  L2, x before y  l, True, T

Lemmas

false wf, subtype rel wf, no repeats iff, l before wf, member wf, iff wf, rev implies wf, select cons tl, decidable int equal, guard wf, fun-path-induction, length nil, length cons, non neg length, le wf, length wf1, int seg wf, select wf, nat wf, not wf, no repeats wf, fun-path wf, retraction wf